poss:(ES{i}Prop{i'}), T:Type{i}, s:T, i:Id, P:(possible-event{i:l}(poss)Prop{i'}),
R:(possible-event{i:l}(poss)possible-event{i:l}(poss)Prop{i'}), Rs:(TTProp{i'}).
ma-knows{i:l}(poss; i; T; s; P; Rs; R)  Prop{i'} 

latex

Definitions	Type, Prop, t  T, ES, x:AB(x), Id, x:A. B(x), PossibleEvent(poss), K(P)@e, poss-consistent(i;T;s;ev;R), P  Q, Ki(P)@s
Lemmas	poss-consistent wf, es-knows wf, possible-event wf, Id wf, event system wf